$\forall$$T$:Type, $l$:($T$ List), $x$,$y$:$T$. l\_before($x$; $y$; $l$; $T$) $\in$ prop\{i:l\}